$\forall$$A$:Type, $f$:($A$$\rightarrow\mathbb{B}$), $L$:$A$ List. split\_tail($L$ $\mid$ $\forall$$x$.$f$($x$)) $\in$ ($A$ List)$\times$($A$ List)